| Definitions | es-state(es; i),  T, map(f; as), es-hist{i:l}(es;e1;e2), event-info(ds;da), fpf-cap(f; eq; x; z), spreadn(a; x,y,z.t(x;y;z)), list_accum(x,a.f(x;a); y; l), es-info(es;e), es-trans-state-from{i:l}(es;ks;g;z;e1;e2), es-dtype(es; i; x; T), es-locl(es; e; e'), i <z j, i  z j, nth_tl(n;as), hd(l), lelt(i; j; k), ||as||, int_seg(i; j), l[i],   b, subtype(S; T), False, A, A B,  x:A. B(x), ma-valtype(da; k), (x  l), P  Q, es-le(es; e; e'),  e' e.P(e'), alle-at(es; i; e.P(e)), A c B, Rinit-v(x1), Reffect-f(x1), Rinit-discrete(A), Rinit-x(x1), Rinit?(x1), Reffect-discrete(A), guard(T), sq_type(T), ff, Rsends-T(x1), Reffect-T(x1), Rsends-dt(x1), Rpre-a(x1), Rpre-ds(x1), Rpre?(x1), Rsends-ds(x1), Rbframe-L(x1), Rbframe-k(x1), Rbframe?(x1), Rsframe-L(x1), Rsends-knd(x1), Rsends-g(x1), Rsframe-tag(x1), Rsends-l(x1), Rsframe-lnk(x1), Rsframe?(x1), Rsends?(x1), Rrframe-L(x1), Reffect-ds(x1), Rrframe-x(x1), Rrframe?(x1), Raframe-L(x1), Raframe-k(x1), Raframe?(x1), Rframe-L(x1), Reffect-knd(x1), Reffect-x(x1), Rframe-x(x1), Rframe?(x1), Reffect?(x1), tt, t.2, bor(p; q), t.1, (i = j), band(p; q), R-interface-compat(A; B), R-discrete_compat(A; B), R-frame-compat(A; B), R-base-domain(R), eq_bd(p; q), Rda(R), Rds(R), R-loc(R), True, Rnone?(x1), Rplus-right(x1), Rplus-left(x1), Rplus?(x1), if b then t else f fi , Y, R-compat{i:l}(A; B), Knd,   x,y. t(x;y), decl-type{i:l}(ds; x), l_all(L; T; x.P(x)), P Q, P    Q, P Q, x. t(x), top, prop{i:l}, t T, P Q, decl-state(ds), x:A. B(x), es-state-when(es; e), wellfounded{i:l}(A; x,y.R(x;y)), effect-p(es; i; ds; k; T; x; f), frame-p(es; i; T; x; L),  , Unit,  , x(s1,s2), x(s),  , es-when(es; x; e), es-after(es; x; e), R-state-var(i; ds; da; x; T; ks; tr) |
| Lemmas | fpf-sub weakening, fpf-sub-join-left2, subtype-fpf-cap-top, subtype rel transitivity, eqof eq btrue, fpf-cap-single, true wf, squash wf, es-interval-eq2, list accum wf, int-rational, es-val wf, es-state-subtype, es-state-when wf, fpf-ap-equal, fpf-dom wf, fpf-trivial-subtype-top, fpf-join-cap-sq, assert-deq-member, es-kind wf, deq-member wf, es-hist wf, list accum append, es-locl transitivity1, es-hist-last, es-loc-pred, es-after-pred, es-pred-locl, es-pred wf, es-le-iff, es-causl wf, es-locl-wellfnd, assert of null, or functionality wrt iff, assert of bor, non neg length, select member, es-E wf, es-loc wf, es-decls wf, es-isconst wf, null wf3, bor wf, select wf, length wf1, nat wf, es-when wf, es-isrcv wf, es-trans-state-from wf, es-decls-iff, es-vartype wf, es-le-loc, es-after wf, es-locl wf, R-state-var wf, R-implies-rule, fpf-empty-compatible-left, fpf-compatible-symmetry, fpf-compatible-join, R-compat-Rall, R-compat-symmetry, frame-p wf, l all wf2, Rframe wf, Rall wf, R-and-rule, R-frame-rule, IdLnk wf, btrue wf, not wf, bnot wf, not functionality wrt iff, assert of bnot, eqff to assert, assert-eq-knd, Kind-deq wf, fpf-compatible-singles, fpf-compatible-self, Id sq, assert-eq-id, eqtt to assert, iff transitivity, bool wf, eq id wf, decidable equal Kind, event system wf, effect-p wf, decl-type wf, rationals wf, Reffect wf, R-all-rule2, normal-valtype, normal-ds-single, fpf-single wf, normal-ds-join, R-effect-rule, fpf wf, fpf-compatible wf, normal-type wf, lnk wf, ldst wf, Id wf, isrcv wf, assert wf, Knd wf, normal-ds wf, normal-da wf, fpf-join wf, decl-state wf, ma-valtype wf, fpf-cap-single1, fpf-single wf3, id-deq wf, fpf-compatible-join-cap, fpf-cap-join-subtype, subtype rel self, top wf, fpf-cap wf, subtype rel dep function, l member wf |
i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, ks:(Knd List), tr:(k:{(k 
decl-state(ds)
isrcv(k))